Satisfiability modulo theories (SMT) solving and satisfiability (SAT) solving may allow a computer to reason about systems and computations symbolically. SMT and SAT solving may be used in software verification, symbolic analysis, program verification, automatic testing, security checking, and the like. SAT solving may include determining whether a model of a propositional formula exists such that the formula evaluates as TRUE. SMT solving may include SAT solving in which propositional variables of the SAT problem are replaced with formulas of another mathematical theory.
To perform SMT solving and SAT solving, some methods and systems may employ the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. The DPLL algorithm is a backtracking-based search algorithm for deciding SAT of propositional logic formulae. Theory solvers may be used with the DPLL algorithm to perform SMT solving. Additional methods and systems have been developed that may improve the performance of the DPLL algorithm. For example, the DPLL may be adapted to employ backjumping, restarting, and/or clause learning.
Efficiency in SMT and SAT solving may remain a significant obstacle, however, particularly when attempting to solve increasingly large problems.